$\forall$$T$:Type, $X$:MaInterface(Top + $T$), ${\it es}$:ES.
\\[0ex]ma{-}interface{-}consistent(${\it es}$;$X$)
\\[0ex]$\Rightarrow$ ([[ma{-}interface{-}right($X$)]] = es{-}interface{-}right([[$X$]]) $\in$ AbsInterface($T$))